A generic framework: from modeling to code
Identifieur interne : 002780 ( Main/Exploration ); précédent : 002779; suivant : 002781A generic framework: from modeling to code
Auteurs : Dominique Méry [France] ; Neeraj Kumar Singh [France]Source :
- Innovations in Systems and Software Engineering [ 1614-5046 ] ; 2011-12-01.
English descriptors
Abstract
Abstract: Model-driven development (MDD) is a very popular technique in the area of software development, but this technique is criticized due to lack of a formal semantics. MDD is used for large-scale system development using semi-formal techniques like UML (Unified Modeling Language), which are not amenable to formal analysis and consistency checking. Formal methods with MDD may provide an assurance of correctness of the system. This paper advocates an approach to building generic framework for rigorous MDD that is based on combining semi-formal notations with formal modeling languages, correctness of the system using model checker and automatic code generation from the verified formal specification. The main objective of this work is to apply model-driven techniques and tools with formal verification and its code generation for designing critical systems. An assessment of the proposed framework is given through a case study, relative to the development of a cardiac pacemaker system.
Url:
DOI: 10.1007/s11334-011-0165-0
Affiliations:
- France
- Grand Est, Lorraine (région)
- Nancy, Vanœuvre-lès Nancy
- Centre national de la recherche scientifique, Institut national de recherche en informatique et en automatique, Laboratoire lorrain de recherche en informatique et ses applications, Mosel (Loria), Université de Lorraine
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 002067
- to stream Istex, to step Curation: 002040
- to stream Istex, to step Checkpoint: 000680
- to stream Main, to step Merge: 002822
- to stream Main, to step Curation: 002780
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">A generic framework: from modeling to code</title><author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name><affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="region" nuts="2">Lorraine (région)</region></placeName><orgName type="team" n="7">Mosel (Loria)</orgName><orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName><orgName type="university">Université de Lorraine</orgName><orgName type="EPST">Centre national de la recherche scientifique</orgName><orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName></affiliation></author><author><name sortKey="Singh, Neeraj Kumar" sort="Singh, Neeraj Kumar" uniqKey="Singh N" first="Neeraj Kumar" last="Singh">Neeraj Kumar Singh</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:8CE3D7DE530BA45704D586A1D55A42657BFC5ECC</idno><date when="2011" year="2011">2011</date><idno type="doi">10.1007/s11334-011-0165-0</idno><idno type="url">https://api.istex.fr/ark:/67375/VQC-VK87CXC7-8/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">002067</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002067</idno><idno type="wicri:Area/Istex/Curation">002040</idno><idno type="wicri:Area/Istex/Checkpoint">000680</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000680</idno><idno type="wicri:doubleKey">1614-5046:2011:Mery D:a:generic:framework</idno><idno type="wicri:Area/Main/Merge">002822</idno><idno type="wicri:Area/Main/Curation">002780</idno><idno type="wicri:Area/Main/Exploration">002780</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">A generic framework: from modeling to code</title><author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>Univesité Henri Poincaré Nancy 1, LORIA, BP 239, 54506, Vanœuvre-lès Nancy</wicri:regionArea><placeName><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region><settlement type="city">Vanœuvre-lès Nancy</settlement></placeName><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="region" nuts="2">Lorraine (région)</region></placeName><orgName type="team" n="7">Mosel (Loria)</orgName><orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName><orgName type="university">Université de Lorraine</orgName><orgName type="EPST">Centre national de la recherche scientifique</orgName><orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="region" nuts="2">Lorraine (région)</region></placeName><orgName type="team" n="7">Mosel (Loria)</orgName><orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName><orgName type="university">Université de Lorraine</orgName><orgName type="EPST">Centre national de la recherche scientifique</orgName><orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName></affiliation></author><author><name sortKey="Singh, Neeraj Kumar" sort="Singh, Neeraj Kumar" uniqKey="Singh N" first="Neeraj Kumar" last="Singh">Neeraj Kumar Singh</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>Univesité Henri Poincaré Nancy 1, LORIA, BP 239, 54506, Vanœuvre-lès Nancy</wicri:regionArea><placeName><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region><settlement type="city">Vanœuvre-lès Nancy</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author></analytic><monogr></monogr><series><title level="j">Innovations in Systems and Software Engineering</title><title level="j" type="sub">A NASA Journal</title><title level="j" type="abbrev">Innovations Syst Softw Eng</title><idno type="ISSN">1614-5046</idno><idno type="eISSN">1614-5054</idno><imprint><publisher>Springer-Verlag</publisher><pubPlace>London</pubPlace><date type="published" when="2011-12-01">2011-12-01</date><biblScope unit="volume">7</biblScope><biblScope unit="issue">4</biblScope><biblScope unit="page" from="227">227</biblScope><biblScope unit="page" to="235">235</biblScope></imprint><idno type="ISSN">1614-5046</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">1614-5046</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Event-B</term><term>Model-driven development (MDD)</term><term>Proof-based refinement and code generation</term><term>UML-B</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: Model-driven development (MDD) is a very popular technique in the area of software development, but this technique is criticized due to lack of a formal semantics. MDD is used for large-scale system development using semi-formal techniques like UML (Unified Modeling Language), which are not amenable to formal analysis and consistency checking. Formal methods with MDD may provide an assurance of correctness of the system. This paper advocates an approach to building generic framework for rigorous MDD that is based on combining semi-formal notations with formal modeling languages, correctness of the system using model checker and automatic code generation from the verified formal specification. The main objective of this work is to apply model-driven techniques and tools with formal verification and its code generation for designing critical systems. An assessment of the proposed framework is given through a case study, relative to the development of a cardiac pacemaker system.</div></front></TEI><affiliations><list><country><li>France</li></country><region><li>Grand Est</li><li>Lorraine (région)</li></region><settlement><li>Nancy</li><li>Vanœuvre-lès Nancy</li></settlement><orgName><li>Centre national de la recherche scientifique</li><li>Institut national de recherche en informatique et en automatique</li><li>Laboratoire lorrain de recherche en informatique et ses applications</li><li>Mosel (Loria)</li><li>Université de Lorraine</li></orgName></list><tree><country name="France"><region name="Grand Est"><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name></region><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name><name sortKey="Singh, Neeraj Kumar" sort="Singh, Neeraj Kumar" uniqKey="Singh N" first="Neeraj Kumar" last="Singh">Neeraj Kumar Singh</name><name sortKey="Singh, Neeraj Kumar" sort="Singh, Neeraj Kumar" uniqKey="Singh N" first="Neeraj Kumar" last="Singh">Neeraj Kumar Singh</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 002780 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 002780 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:8CE3D7DE530BA45704D586A1D55A42657BFC5ECC
|texte= A generic framework: from modeling to code
}}
| This area was generated with Dilib version V0.6.33. |  |